(declare-fun P (Int) Bool)
(declare-fun Q (Bool Int Int Bool Int Int) Bool)
(declare-fun R (Bool Int Int) Bool)
(assert (not (exists ((v1 Int)) (P v1))))
(assert (forall ((v1 Int) (v2 Int) (v3 Bool) (v4 Int) (v5 Int) (v6 Int)) (=> (and (Q v3 v4 v2 true v5 v6) (>= v2 1)) (P v1))))
(assert (forall ((v1 Bool) (v2 Int) (v3 Int) (v4 Bool) (v5 Int) (v6 Int) (v7 Int) (v8 Bool) (v9 Int) (v10 Int)) (=> (and (Q v8 v9 v7 v1 v2 v10) (= (+ 1 v3) v7) (>= v7 1) (= v5 v2) (not v1) (not v4)) (Q v1 v2 v3 v4 v5 v6))))
(assert (forall ((v1 Bool) (v2 Int) (v3 Int) (v4 Int) (v5 Bool) (v6 Int) (v7 Int)) (=> (and (R v5 v6 v4) (Q v5 v6 v4 v1 v2 v7) (>= v4 1) (= (+ 1 v3) v4) (not v1)) (R v1 v2 v3))))
(assert (forall ((v1 Bool) (v2 Int) (v3 Int) (v5 Bool) (v6 Int) (v7 Int)) (=> (and (not v5)) (Q v1 v2 v3 v5 v6 v7))))
(assert (forall ((v1 Bool) (v2 Int) (v3 Int)) (=> (and (not v1)) (R v1 v2 v3))))
(check-sat)
